\begin{tabbing}
$\forall$$D$:Dsys.
\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ (\=$\exists$${\it dec}$:($j$,$b$:Id$\rightarrow$M($j$).state$\rightarrow$(M($j$).da(locl($b$))+Unit)).\+
\\[0ex](\=$\forall$$j$, $x$, $b$:Id.\+
\\[0ex]$\neg$M($j$).rframe(locl($b$) reads $x$)
\\[0ex]$\Rightarrow$ ($\forall$$s_{1}$, $s_{2}$:M($j$).state. ($s_{1}$ $\equiv$ $s_{2}$ mod $x$) $\Rightarrow$ ${\it dec}$($j$,$b$,$s_{1}$) $=$ ${\it dec}$($j$,$b$,$s_{2}$)))
\-\\[0ex]\& d{-}chooser($D$;${\it dec}$))
\-
\end{tabbing}